package karpiel.boguchwal.wojciech.przemek

import karpiel.boguchwal.wojciech.przemek.Ast._
import org.scalatest.FunSuite


class NoDepsParserTest extends FunSuite {
  test("parse") {
    implicit val cache: Cache = RealCache()
    assert(NoDepsParser.parse("(Bruijn 0)").expression == Bruijn(0))
    assert(
      Bruinizer.bruinize(
        NoDepsParser.parse("(sum Bool (Pi (x Unit) tt))").expression)(Context.Empty, implicitly) == SumType(BoolType, PiType(UnitType, UnitValue)))
  }

  test("common -readme") {
    implicit val cache: Cache = RealCache()

    new CommonParsingCases(NoDepsParser.parse(_).expression).readMeCases()
      .foreach { case (a, b) => assert(a == b) }
  }

  test("nat") {
    implicit val cache: Cache = RealCache()
    new CommonParsingCases(NoDepsParser.parse(_).expression).nat()
      .foreach { case (a, b) => assert(a == b) }
  }

  test("nat-double") {
    implicit val cache: Cache = RealCache()

    val pp = NoDepsParser.parse(
      scala.io.Source.fromFile("Nat.prmk").mkString
    )
    val b = Bruinizer.bruinize(pp.expression)(pp.initalContext, implicitly)
    val bnotm = b.normalized(pp.initalContext, implicitly)

    assert(bnotm == StdLib.Nat.double.normalized(Context.Empty, implicitly))
    //additional checks
    implicit val ctx: Context = pp.initalContext
    assert(Bruinizer.bruinize(Var("zero")).normalized == Bruinizer.bruinize(Var("zero-xD")).normalized)
    assert(Bruinizer.bruinize(Var("one")).normalized == StdLib.Nat.one)
    assert(Bruinizer.bruinize(Var("two")).normalized == PiElim(StdLib.Nat.succ, StdLib.Nat.one).normalized(Context.Empty, implicitly))
    assert(Bruinizer.bruinize(Var("two")).normalized == PiElim(StdLib.Nat.double, StdLib.Nat.one).normalized(Context.Empty, implicitly))
    assert(Bruinizer.bruinize(Var("four")).normalized == PiElim(StdLib.Nat.double, PiElim(StdLib.Nat.succ, StdLib.Nat.one)).normalized(Context.Empty, implicitly))
    assert(Bruinizer.bruinize(Var("four")).normalized == PiElim(StdLib.Nat.succ, PiElim(StdLib.Nat.succ, PiElim(StdLib.Nat.succ, StdLib.Nat.one))).normalized(Context.Empty, implicitly))
    //sanity
    assertThrows[Exception](Bruinizer.bruinize(Var("four")).assertEquals(Bruinizer.bruinize(Var("two"))))
    assertThrows[Exception](Bruinizer.bruinize(Var("xD")))
  }

  test("init ctx") {
    implicit val cache: Cache = RealCache()
    assert(NoDepsParser.parse(
      "(set my-unit Unit tt)" +
        "(set my-bool false)" +
        "my-unit").initalContext == Context.Empty.append(UnitType, UnitValue, "my-unit").append(BoolType, BoolFalse, "my-bool"))
    assert(NoDepsParser.parse(
      "(set my-unit tt)" +
        "(set my-bool Bool false)" +
        "my-unit").initalContext == Context.Empty.append(UnitType, UnitValue, "my-unit").append(BoolType, BoolFalse, "my-bool"))
    assertThrows[Exception](NoDepsParser.parse(
      "(set my-unit Bool tt)" +
        "my-unit").initalContext)
  }
}
